Inference at * 
Iof proof for Lemma comp id l:


  A, B:Type, f:(AB). (Id{B} o f) = f 

latex

 by Unfold `tidentity` 0 

latex

 1: 

 1:   A, B:Type, f:(AB). (Id o f) = f
 .

Definitions

Id{T}